package joc.nextgen.dbi;

import static joc.nextgen.JOC.result;
import joc.nextgen.dbi.JOC.PostCondition;

public class PointSpecContract implements PointSpec {

	@ClassInvariant
	public void invariant() {
		assert getX() >= 0 : "x >= 0";
		assert getY() >= 0 : "y >= 0";
	}

	@Override
	public int getX() {
		new PostCondition() {
			{
				assert result(int.class) >= 0 : "result >= 0";
			}
		};
		return 0;
	}

	@Override
	public int getY() {
		new PostCondition() {
			{
				assert result(int.class) >= 0 : "result >= 0";
			}
		};
		return 0;
	}

}
